(include-book "doublecheck" :dir :teachpacks)
(include-book "testing" :dir :teachpacks)
(include-book "io-utilities" :dir :teachpacks)
(include-book "list-utilities" :dir :teachpacks)
(include-book "driver")

; Replace function should return equal length list
(defproperty replace-returns-equal-length-list
  (xs    :value (random-list-of (random-integer))
   start :value 0
   end   :value (+ start 5)
         :where (and (consp xs) (> (len xs) end)))
  (equal (len (replace start end 0 xs)) (len xs)))

; Round-trip replace
(defproperty replace-round-trip
  (xs    :value (replicate (random-integer) 1)
   start :value 0
   end   :value (+ start 5)
         :where (and (consp xs) (> (len xs) end)))
  (equal (replace start end 1 (replace start end 0 xs)) xs))

; Helper function for count
(defun count-helper (char-list char acc)
  (if (consp char-list)
      (if (equal (car char-list) char)
          (count-helper (cdr char-list) char (+ acc 1))
          (count-helper (cdr char-list) char acc)
      )
      acc
  )
)

; Counts number of occurences in a string of a character
; Should be intrinsic function of ACL2, but for some reason
; it itsn't
(defun count (char string)
  (let ((char-list (str->chrs string)))
    (count-helper char-list char 0)
  )
)

; Trim strings shouldn't have spaces
(defproperty trim-stringss-works 
  (string :value (random-list-of (random-char))
          :where (> (len string) 0))
  (equal (count #\space (chrs->str string)) 0))

; Sum function
(defun sum (xs acc)
  (if (consp xs)
      (sum (cdr xs) (+ acc (car xs)))
      acc
  )
)

; get-weights should add up to 1
(defproperty get-weights-equals-1
  (weights :value (random-list-of (random-natural))
   spec    :value (list (cons #\a weights) #\b)
           :where (equal (len weights) 4))
  (equal (sum (get-weights spec) 0) 1))
  

; Check expects for incorrect weight input
(check-expect (input-parse-helper (list 1 1 1 1)) "Error!")
(check-expect (input-parse-helper (list 1 1 1)) "Error!")
(check-expect (input-parse-helper (list 1 1)) "Error!")
(check-expect (input-parse-helper (list 1 1 1 1 1 1 1 1 1 1)) "Error!")

; Check expects for map-day-of-week-to-number
(check-expect (map-day-of-week-to-number #\U) 0)
(check-expect (map-day-of-week-to-number #\R) 4)
(check-expect (map-day-of-week-to-number #\X) #\X)
